$\forall$$T$:Type, $b$:$\mathbb{B}$, $x$,$y$:$T$. ($\neg$($\uparrow$$b$)) $\Rightarrow$ (if $b$ then $x$ else $y$ fi  = $y$)